UnequalSorts.agda:8,7-11
One' !=< One of type Set₁
when checking that the expression one' has type One
